IdrisのIDE Protocol

https://gyazo.com/44b86836c26e1625cb7721a8a82f504f

code:idr

my_v|ect_map : (a -> b) -> Vect n a -> Vect n b -- ①Generate an initial pattern match clause

my_vect_map : (a -> b) -> Vect n a -> Vect n b

my_vect_map f x|s = ?my_vect_map_rhs -- ②Generate a case split for a pattern variable

my_vect_map : (a -> b) -> Vect n a -> Vect n b

my_vect_map f [] = ?my_vect|_map_rhs_1 -- ③Attempt to fill out holes by proof search

my_vect_map f (x :: y) = ?my|_vect_map_rhs_2 -- ③Attempt to fill out holes by proof search

-- 最終

my_vect_map : (a -> b) -> Vect n a -> Vect n b

my_vect_map f [] = []

my_vect_map f (x :: y) = f x :: my_vect_map f y

実装

REPLの中に関数がある

どういう実装か

型ありきなのか